Nuprl Lemma : w-machine_wf
11,40
postcript
pdf
w
:World,
i
:Id. w-machine(
w
;
i
)
w-automaton(
w
.T(
i
);
w
.TA(
i
);
w
.M)
latex
Definitions
w-automaton(
T
;
TA
;
M
)
,
x
:
A
B
(
x
)
,
World
,
x
:
A
B
(
x
)
,
w
.T
,
w
.TA
,
w
.M
,
w-machine(
w
;
i
)
,
x
:
A
.
B
(
x
)
,
f
(
a
)
,
t
T
,
Id
Lemmas
Id
wf
,
world
wf
origin
w:World, i:Id. w-machine(w;i) 
w-automaton(w.T(i);w.TA(i);w.M) w:World, i:Id. w-machine(w;i) w-automaton(w.T(i);w.TA(i);w.M) 
B(x)
B(x)x:A. B(x) T